The language syntax structures are listed as follows. The complete grammar rules can be found in Section 3.3.1.3.

3.1.1.1 Global Definitions (this part is same as CSP module)

3.3.1.1 Probability Processes (this part extends CSP module with probabilistic behaviors)

• pcase

3.3.1.2 Assertions (this part extends CSP module)

• Deadlock free with probability 
• Reachability with probability
• LTL with probability